package org.korifey.ffbdd.impl;

import java.util.Iterator;
import java.util.List;

import org.korifey.ffbdd.api.IBdd;
import org.korifey.ffbdd.api.IBddBackend;
import org.korifey.ffbdd.api.IBddDomain;
import org.korifey.ffbdd.api.INode;
import org.korifey.ffbdd.api.INonterminal;
import org.korifey.ffbdd.api.ITerminal;
import org.korifey.ffbdd.api.ITraverseStrategy;
import org.korifey.ffbdd.api.deprecated.Bdd;
import org.korifey.ffbdd.api.op.IBinaryOperation;
import org.korifey.ffbdd.api.op.IOpCache;
import org.korifey.ffbdd.api.op.IUnaryOperation;
import org.korifey.ffbdd.api.op.OpCacheKey;
import org.korifey.ffbdd.api.op.OperationEnum;
import org.korifey.ffbdd.api.traverse.DependantVarsStrategy;
import org.korifey.ffbdd.api.traverse.NodeAccStrategy;

import static org.korifey.ffbdd.api.util.NodeUtil.*;
import static org.korifey.ffbdd.common.util.ArrayUtil.*;
import static org.korifey.ffbdd.common.util.IntUtil.*;

public class ROBDD<T> implements IBdd<T> {

	private INode root;	
	private BddDomainImpl domain; 
	
	protected ROBDD(INode n, BddDomainImpl domain) {
		root = n;
		this.domain = domain;
	}
	
	@Override
	public BddDomainImpl getDomain() {	
		return domain;
	}
	
	public IOpCache getOpcache() {
		return domain.getOpCache();
	}
	
	public IBddBackend getBackend() {
		return domain.getBackend();
	}
	
	//Node creation	
	protected <E> ITerminal<E> insertTerminal(E value) {
		return getBackend().insertTerminal(value);
	}
	
	protected INode insertNonterminal(int var, INode one, INode zero) {
		return getBackend().insertNonterminal(var, one, zero);
	}

	
	@Override
	public int hashCode() {
		final int prime = 31;
		int result = 1;
		result = prime * result + ((domain == null) ? 0 : domain.hashCode());
		result = prime * result + ((root == null) ? 0 : root.hashCode());
		return result;
	}

	@Override
	public boolean equals(Object obj) {
		if (this == obj)
			return true;
		if (obj == null)
			return false;
		if (getClass() != obj.getClass())
			return false;
		ROBDD other = (ROBDD) obj;
		if (domain == null) {
			if (other.domain != null)
				return false;
		} else if (!domain.equals(other.domain))
			return false;
		if (root == null) {
			if (other.root != null)
				return false;
		} else if (!root.equals(other.root))
			return false;
		return true;
	}
	
	@Override
	public INode getRoot() {
		return root;
	}
	
	@Override
	public <E> IBdd<E> applyUnary(IUnaryOperation<T, E> op) {
		return new ROBDD(_applyUnary(root, op), getDomain());
	}
	
	private <T, E> INode _applyUnary(INode n, IUnaryOperation<T, E> op) {
		OpCacheKey key = new OpCacheKey.Unary(n, op.code()); 
		INode res = getOpcache().get(key);
		if (res != null) return res;
		
		if (n.isTerm()) res = insertTerminal(op.apply(((ITerminal<T>)n).getValue()));
		else {
			INonterminal nn = (INonterminal) n; 
			res = insertNonterminal(nn.var(), _applyUnary(nn.one(), op), _applyUnary(nn.zero(), op)); 
		}
		getOpcache().put(key, res);
		return res;
	}
	

	@Override
	public IBdd<T> injectElement(T value, int[] varIndex, boolean[] varValue) { 
		IBdd<Boolean> elem = domain.makeConst(true);
		for (int i=0; i<varIndex.length; i++) {
			elem = domain.applyBinary(elem, domain.makeNode(varIndex[i], true, false, varValue[i]), (IBinaryOperation)OperationEnum.AND.getOperation());
		}
		return domain.ite(elem, domain.makeConst(value), this);
	}

	@Override
	public IBdd<T> injectNewElements(List<T> values) {
		int size = values.size();
		int domlen = log2(size);
		int[] varidx = new int[domlen];
		boolean[] varval = new boolean[domlen];
		
		for (int i=0; i<domlen; i++) varidx[i] = domain.acuireFreeVar();
		
		IBdd<T> res = this;
		for (int i=0; i<size; i++) {
			res = res.injectElement(values.get(i), varidx, varval);
			increment(varval);
		}
		return res;
	}

	@Override
	public boolean isConst() {
		return root.isTerm();
	}
	
	public void mark() {
		_mark(root);
	}
	
	public void unmark() {
		_unmark(root);
	}
	
	

	@Override
	public List<Integer> dependantVariables() {
		DependantVarsStrategy strategy = new DependantVarsStrategy();
		traverse(strategy);
		return strategy.getAccumulated();
	}


	public List<INode> listNodes() {
		NodeAccStrategy strategy = new NodeAccStrategy();
		traverse(strategy);
		return strategy.getAccumulated();
	}
	
	public void traverse(ITraverseStrategy strategy) {
		_traverse(getRoot(), strategy);
		unmark();
	}
	
	private static void _traverse(INode n, ITraverseStrategy strategy) {
		strategy.proccess(n);
		n.setMark(true);
		if (!n.isTerm()) {
			INonterminal nt = (INonterminal)n;
			if (!nt.one().isMarked()) _traverse(nt.one(), strategy);
			if (!nt.zero().isMarked()) _traverse(nt.zero(), strategy);
		}
	}
	

	
	public static class RestrictOperation implements Runnable {
		private int[] varIndex;
		private boolean[] varValue;
		private INode result = null;
		private INode root;
		
		public RestrictOperation(INode root, int[] varIndex, boolean[] varValue) {
			this.root = root;
			this.varIndex = varIndex;
			this.varValue = varValue;
		}
		
		public INode getResult() {
			return result;
		}
		
		private INode inner(INode n) {
			return null;
		}
		
		public void run() {
			result = inner(root);
		}
	}
	
	
	@Override
	public IBdd<T> restrict(int[] varIndex, boolean[] varValue) {
		// TODO Auto-generated method stub
		return null;
	}

	
	@Override
	public List<boolean[]> solveEquation(T value, int[] varIndex,
			ITraverseStrategy strategy) {
		// TODO Auto-generated method stub
		return null;
	}

	
	@Override
	public IBdd<T> rename(int[] oldIndex, int[] newIndex) {
		// TODO Auto-generated method stub
		return null;
	}

	
	@Override
	public IBdd<T> substitute(IBdd<T> replacement, T replacable) {
		// TODO Auto-generated method stub
		return null;
	}
	

}
